FDL - Step of Proof: connex_functionality_wrt

Step of Proof: connex_functionality_wrt_iff

12,41

Inference at *
Iof proof for Lemma connex functionality wrt iff:

T:Type, R, R':(T

(

x, y:T. R(x,y)

R'(x,y))

(Connex(T;x,y.R(x,y))

Connex(T;x,y.R'(x,y)))

by ((((UnivCD)

CollapseTHENM (Unfold `connex` 0))

)

CollapseTHENA ((Auto_aux (first_nat 1:n

C) ((first_nat 1:n),(first_nat 3:n)) (first_tok :t) inil_term)))

C1:

C1: 1. T : Type

C1: 2. R : T

C1: 3. R' : T

C1: 4.

x, y:T. R(x,y)

R'(x,y)

C1:

(

x, y:T. R(x,y)

R(y,x))

(

x, y:T. R'(x,y)

R'(y,x))

Definitions P Q, P & Q, t T, Connex(T;x,y.R(x;y)), x(s1,s2), P Q, P Q, , x:A. B(x)

Lemmas iff wf

Definitions	P Q, P & Q, t T, Connex(T;x,y.R(x;y)), x(s1,s2), P Q, P Q, , x:A. B(x)
Lemmas	iff wf